k:Knd, T:Type, l:IdLnk, ds, dt:tg:Id fp Type,
g:((tg:Id  (State(ds)T(DeclaredType(dt;tg) List))) List).
((isrcv(k))  (lnk(k) = l)  (T = DeclaredType(dt;tag(k))))
 ((isrcv(k))  (destination(lnk(k)) = source(l)  Id))
 Normal(ds)
 Normal(T)
 Normal(dt)
 es.sends k(v:T) on l:
 es.tagged(g,State(ds),v):dt 

latex

Definitions	suptype(S; T), S  T, x. t(x), , P & Q, t  T, x:A. B(x), es.P(es), P  Q, x:A. B(x), P  Q, x(s), DeclaredType(ds;x)
Lemmas	assert-eq-lnk, Knd wf, fpf wf, tagof wf, IdLnk wf, lsrc wf, ldst wf, Id wf, isrcv wf, normal-type wf, normal-ds wf, event system wf, decl-type wf, id-deq wf, fpf-cap wf, decl-state wf, sends-p wf, R-realizes wf, lnk wf, eq lnk wf, assert wf, R-sends-rule, Rsends wf